module fn.logic.fol.syntax.Formula

open fn.adt.Tree
open fn.pattern.functor_.Operators


type Kinds = Predicate | Function | Connective | Unknown

(*
 * Identifier is the building block for first-order formulas. It inhabits
 * all the values in the nodes of the formula's expression tree.
 *)
[<CustomEquality;CustomComparison>]
type Identifier = 
    { literal : obj; kind : Kinds }
    static member make s = { literal=s; kind=Unknown }
    override this.ToString() = this.literal.ToString()
    static member op_Implicit (s : string) = Identifier.make s
    (* all this just to have Map<Identifier,_>. Sheesh. *)
    member this.structure() = (this.literal.ToString(), this.kind)
    override this.Equals(other: obj) =
        match other with
        | :? Identifier as y -> 
            if this.kind = Unknown || y.kind = Unknown
                then (this.literal = y.literal)
                else (this.structure() = y.structure())
        | _ -> (this.ToString() = other.ToString())
    override this.GetHashCode() = hash this.literal
    interface System.IComparable with
        member this.CompareTo other =
            match other with
            | :? Identifier as y when this.kind <> Unknown && y.kind <> Unknown ->
                compare (this.structure()) (y.structure())
            | _ -> compare (this.ToString()) (other.ToString())

          
let (|Literal|_|) (s : 'a) (i : Identifier) = 
    if i.literal=(s:>obj) then Some() else None

(*
 * A signature is a collection of identifiers with properties
 *)
type FolSignature (symbols : Map<Identifier, int>) =
    member this.symbols = symbols
    
    member this.enkind (identifier : Identifier) =
        if identifier.kind = Unknown then
            match Map.tryFindKey (fun k v -> k.literal=identifier.literal) symbols with
            | Some matching_identifier -> matching_identifier
            | None -> identifier
        else
            identifier
    
    member this.enkind (e : Tree<Identifier>) =
        match e with
        | Node(r, sub) -> Node(this.enkind r, [for s in sub -> this.enkind s])
        
(*
 * A formula is essentially a tree of identifiers.
 *)
type FolFormula<'I when 'I : equality and 'I : comparison> (e: Tree<'I>) =
    
    let (|Node|) (fa : FolFormula<_>) =
        match fa.e with
        | Node(a,b) -> (a,[for x in b -> FolFormula x])

    member this.e = e

    static member PREFIXES = Map.ofList ["-", 6; "~", 5]
    static member INFIXES = Map.ofList ["&", 2; "=", 3; ":", 1; ">", 3; "<", 3;
                                        "+", 4; "-", 4; "*", 5; "/", 5; "%", 5; "^", 6;
                                        "∩", 5; ":∈ ", 3]

    static member INTRINSICS = 
        let l = [{ literal="&"; kind=Connective }, 2]
        FolSignature (Map.ofList l)

    static member atom (r : 'I) = FolFormula<'I>(Node (r,[]))

    static member node (r : 'I) (sub : FolFormula<'I> list) = FolFormula<'I>(Node (r,[for s in sub -> s.e]))

    member this.subexpr i = FolFormula<'I>(this.e.subtrees.[i]);
    member this.subexprs = Seq.toArray this.e.subtrees

    member this.split(symbol : 'I) = [for e in (this.e.split symbol) -> FolFormula(e)]
    member this.split() =
        match FolFormula<'I>.AND :> obj with
        | :? 'I as x -> this.split x
        | _ -> failwith "Required argument for FolFormula<...>.split" 

    static member join (symbol : 'I) (parts : FolFormula<'I> seq) =
        Seq.reduce (fun x y -> FolFormula.node symbol [x;y]) parts 

    override this.ToString() =
        match this with
        | Node(x, [a;b]) 
            when FolFormula<_>.INFIXES.ContainsKey(x.ToString()) ->
                let enparen (Node(y, _) as el : FolFormula<'I>) = 
                    match FolFormula<_>.INFIXES.TryFind(y.ToString()) with
                    | Some prio -> sprintf "(%O)" el
                    | None -> el.ToString()
                sprintf "%s %O %s" (enparen a) x (enparen b)
        | Node(r, []) -> r.ToString()
        | Node(r, sb) -> sprintf "%O(%s)" r ([|for s in sb -> s.ToString()|] |> String.concat ",")
    
    (* Global constants *)
    static member AND = {literal="&"; kind=Connective}
    
    (* all this just to have Map<FolFormula,_>. Sheesh. *)
    member this.structure() = (this.e)
    override this.Equals(other: obj) =
        match other with
        | :? FolFormula<'I> as y -> (this.structure() = y.structure())
        | _ -> false
    override this.GetHashCode() = hash (this.structure())
    interface System.IComparable with
        member this.CompareTo other =
            match other with
            | :? FolFormula<'I> as y -> compare (this.structure()) (y.structure())
            | _ -> failwith "uncomparable: %O and %O" this other


type FolFormula = FolFormula<Identifier>


type FolSignature with
    member this.enkind (phi : FolFormula<Identifier>) =
        FolFormula<Identifier> (this.enkind phi.e)

    static member ( |@ ) (anything : FolFormula, signature : FolSignature) = signature.enkind anything


let (|Node|) (fa : FolFormula<'I>) =
    match fa.e with
    | Node(a,b) -> (a,[for x in b -> FolFormula<'I> x])
